Gate-level logic simulation is used extensively to verify the correctness of design netlists. Typically, input stimuli are applied to the netlist, and the simulation results are compared with a golden model or pre-defined checkers. When unknown values (Xs) exist, however, gate-level simulation can no longer produce correct results due to X-pessimism. FIG. 2 shows a classical example of a logical false X: the output of gate g4 should be 1 but logic simulation produces X instead. Such inaccuracy can produce numerous false Xs, rendering gate-level simulation useless. This problem is becoming severe due to physical optimizations and low-power requirements that allow Xs to exist in the design.
To eliminate logical false Xs, the SimXACT technique (U.S. Pat. No. 8,402,405) formally analyzes an input trace to find fixes that can eliminate all combinational false Xs encountered during the simulation of the trace. The inputs to SimXACT are a trace as input stimuli, a gate-level netlist, and a start time that the Xs should be checked for the first time to determine whether they are false or not. The output is auxiliary code that when the same X-pessimism conditions are encountered, those false Xs will be replaced with the correct values.
After the analysis of the trace is finished, the generated auxiliary code can be used with future simulation to eliminate the false Xs. This flow allows gate-level simulation to produce correct results.
SimXACT analysis is comprehensive and is guaranteed to produce correct simulation results that match real hardware. However, it only solves X-pessimism caused by logical false Xs. Another source of false Xs come from modeling of sequential elements for logic simulation. Take FIG. 3 for example, for a Flip-Flop (FF), if its clock is X and data input has changes, should the output be corrupted to X? In zero-delay simulation it is common that all clocks toggle at the same time and FF outputs changes accordingly. Given that the X at the clock of the FF may actually have an X→X change (in other words, it could be either 0→1 or 1→0 but no transition is detected by the FF because X→X does not create a transition in simulation), if the data input has changes the output may indeed need to be updated. Thus the modeling of FFs may conservatively corrupt the output of the FF to X when it sees changes at its data input and X at the clock pin. However, if the X is a stable 0 or 1 instead of an X→X transition, the output of the FF should not change, and the X corruption will create a false X that can corrupt more circuit elements in downstream logic, producing simulation results that are full of false Xs and difficult to analyze.